$\forall$${\it es}$:ES, $e$, $a$:E.
\\[0ex]$a$ $\leq$loc $e$ 
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$first($a$)))
\\[0ex]$\Rightarrow$ (es{-}le{-}before(${\it es}$;$e$) = (es{-}le{-}before(${\it es}$;pred($a$)) @ [$a$, $e$]) $\in$ (E List))